Skip to content

Fix filename completion in bash autocompletion #8587

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
merged 1 commit into from
Apr 4, 2025
Merged

Fix filename completion in bash autocompletion #8587

merged 1 commit into from
Apr 4, 2025

Conversation

tautschnig
Copy link
Collaborator

Bash globbing does not support | for alternatives, which meant that the prior pattern would only match file names that contained a |.

  • Each commit message has a non-empty body, explaining why the change was made.
  • n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
  • n/a My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

@tautschnig tautschnig requested a review from a team as a code owner February 9, 2025 22:45
@codecov Codecov
Copy link

codecov bot commented Feb 9, 2025 •
edited
Loading

Codecov Report

All modified and coverable lines are covered by tests ✅

Project coverage is 80.37%. Comparing base (41e9f3d) to head (1e71b4d).
Report is 4 commits behind head on develop.

Additional details and impacted files 
@@             Coverage Diff             @@
##           develop    #8587      +/-   ##
===========================================
- Coverage    80.38%   80.37%   -0.01%     
===========================================
  Files         1686     1686              
  Lines       206770   206770              
  Branches        85       85              
===========================================
- Hits        166207   166198       -9     
- Misses       40563    40572       +9

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:
  • ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
  • 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

@tautschnig
Fix filename completion in bash autocompletion
1e71b4d 
Bash globbing does not support `|` for alternatives, which meant that
the prior pattern would only match file names that contained a `|`.
@tautschnig tautschnig force-pushed the fix-bash-completion branch from 7541547 to 1e71b4d Compare April 4, 2025 08:06
@tautschnig tautschnig merged commit 0dc8704 into diffblue:develop Apr 4, 2025
40 checks passed
@tautschnig tautschnig deleted the fix-bash-completion branch April 4, 2025 21:38
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@peterschrammel peterschrammel peterschrammel approved these changes

Assignees

@peterschrammel peterschrammel

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@tautschnig @peterschrammel